theory Design_Sec_InvokeCommand imports "../Design_Instantiation" begin section "auxiliary lemma" lemma Driver_Read_not_change_old: "∀s. (⇑(Driver_Read s smc_ex_init_read zx_mgr)) = ⇑s" using Driver_Read_def by simp lemma Driver_Write_smc_not_change_old: "∀s. (⇑(fst(Driver_Write_smc s zx_mgr ZX_OKr smc_ex_init))) = (⇑s)" using Driver_Write_smc_def by auto lemma tee_invokeTACommand_TEEDomain2R_notchnew: assumes p1: "s'=(fst (tee_invokeTACommand_TEEDomain2R sc s ses_id time_out cmd_id in_params out_params))" shows "(s ∼. d .∼Δ s')" using tee_invokeTACommand_TEEDomain2R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_InvokeTACommand1R_notchnew: assumes p1: "s'=(fst(TEE_InvokeTACommand1R sysconf s memBlock_memRef))" shows "(s ∼. d .∼Δ s')" using TEE_InvokeTACommand1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_InvokeTACommand2R_notchnew: assumes p1: "s'=(fst(TEE_InvokeTACommand2R sysconf s))" shows "(s ∼. d .∼Δ s')" using TEE_InvokeTACommand2R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_InvokeTACommand4R_notchnew: assumes p1: "s'=(fst(TEE_InvokeTACommand4R sysconf s))" shows "(s ∼. d .∼Δ s')" using TEE_InvokeTACommand4R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TA_InvokeCommandEntryPoint_refine : "∀s. (TA_InvokeCommandEntryPoint sc (⇑s) opt tid) = ⇑(TA_InvokeCommandEntryPointR sc s opt tid)" using TA_InvokeCommandEntryPoint_def TA_InvokeCommandEntryPointR_def abstract_state_def abstract_state_rev_def by simp lemma abs_rev_lemma:"(⇑(s⇓t)) =t" by auto lemma mgr_ta_sessions_findSesServTid: "∀s t ses_id ses_id_t. ses_id = ses_id_t ∧ mgr_ta_sessions (ta_mgr (TEE_state s)) = mgr_ta_sessions (ta_mgr (TEE_state t)) ⟶ findSesServTid s ses_id = findSesServTid t ses_id_t" proof- { fix s::"State" fix t::"State" fix ses_id::"SESSION_ID_TYPE" fix ses_id_t::"SESSION_ID_TYPE" let ?mgrTaSesList = "mgr_ta_sessions (ta_mgr (TEE_state s))" let ?mgrTaSes = "findTaSesInMgrBySesId ?mgrTaSesList ses_id" let ?mgrTaSesList_t = "mgr_ta_sessions (ta_mgr (TEE_state t))" let ?mgrTaSes_t = "findTaSesInMgrBySesId ?mgrTaSesList_t ses_id_t" assume a1: "ses_id = ses_id_t" assume a2: "mgr_ta_sessions (ta_mgr (TEE_state s)) = mgr_ta_sessions (ta_mgr (TEE_state t))" have b1: "?mgrTaSesList = ?mgrTaSesList_t" by (simp add: a2) have b2: "ses_id = ses_id_t" by (simp add: a1) have b3: "?mgrTaSes = ?mgrTaSes_t" by (simp add: b1 b2) have b4: "findSesServTid s ses_id = findSesServTid t ses_id_t" by (simp add: b3 findSesServTid_def) } then show ?thesis by blast qed section "refinement proof" subsection "TEEC side" lemma TEEC_InvokeCommand1R_refine: "∀s. fst (TEEC_InvokeCommand1 sc (⇑s) ses_id time_out cmd_id in_params out_params memBlock_memRef) = ⇑(fst (TEEC_InvokeCommand1R sc s ses_id time_out cmd_id in_params out_params memBlock_memRef))" using TEEC_InvokeCommand1_def TEEC_InvokeCommand1R_def abstract_state_def abstract_state_rev_def by auto lemma TEEC_InvokeCommand2R_refine: "∀s. fst (TEEC_InvokeCommand2 sc (⇑s)) = ⇑(fst(TEEC_InvokeCommand2R sc s))" proof- { fix s let ?s'="fst(TEEC_InvokeCommand2R sc s)" let ?t = "⇑s" let ?t' = "fst(TEEC_InvokeCommand2 sc ?t)" have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01:"?t' =⇑(?s')" proof- { show ?thesis proof(cases"current s ≠ TEE sc ∨ (exec_prime s) = [] ∨ (snd (hd (exec_prime s)) ≠ TEEC_IC2)") case True have a1: "current s ≠ TEE sc ∨ (exec_prime s) = [] ∨ (snd (hd (exec_prime s)) ≠ TEEC_IC2)" using True by auto have a2:"?t = ?t'" using TEEC_InvokeCommand2_def a1 by (smt (z3) a0 fstI) have a3:"s = ?s'" using TEEC_InvokeCommand2_def a1 by (smt (z3) TEEC_InvokeCommand2R_def fstI) then show ?thesis using a2 a3 by simp next case False have a4: "¬(current s ≠ TEE sc ∨ (exec_prime s) = [] ∨ (snd (hd (exec_prime s)) ≠ TEEC_IC2))" using False by auto then show ?thesis proof- { let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec⦈" let ?s_invoke = "tee_invokeTACommand_TEEDomain2R sc ?s_rev_event ?ses_id ?time_out ?cmd_id ?in_params ?out_params" let ?t_invoke = "tee_invokeTACommand_TEEDomain2 sc ?t_rev_event ?ses_id ?time_out ?cmd_id ?in_params ?out_params" let ?s_state = "fst ?s_invoke" let ?t_state = "fst ?t_invoke" let ?s2 = "Driver_Read ?s_state smc_ex_init_read zx_mgr" let ?s_origin = "fst(snd ?s_invoke)" let ?s_code = "fst(snd (snd ?s_invoke))" let ?s_params = "(snd (snd (snd ?s_invoke)))" have a5: "?t_rev_event = ⇑(?s_rev_event)" by auto have a6: "?t_state = ⇑(?s_state)" using tee_invokeTACommand_TEEDomain2R_def a5 by (metis abs_rev_lemma fstI) have a7: "?t_state = ⇑(?s2)" using Driver_Read_not_change_old a6 by presburger have a8: "?s' = ?s2" using a4 TEEC_InvokeCommand2R_def by (smt (verit) Pair_inject State.unfold_congs(6) prod.exhaust_sel) have a9: "?t' = ?t_state" using a0 a4 TEEC_InvokeCommand2_def by (smt (verit) Pair_inject State.unfold_congs(6) prod.exhaust_sel) show ?thesis using a8 a9 using a7 by presburger } qed qed } qed } then show ?thesis by blast qed lemma TEEC_InvokeCommand3R_refine: "∀s. fst (TEEC_InvokeCommand3 sc (⇑s)) = ⇑(fst(TEEC_InvokeCommand3R sc s))" proof- { fix s let ?s' = "fst(TEEC_InvokeCommand3R sc s)" let ?t = "(⇑s)" let ?t' = "fst (TEEC_InvokeCommand3 sc ?t)" let ?exec = "(exec_prime s)" let ?exec_t = "(exec_prime ?t)" let ?p = "fst (hd ?exec)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id = "param1 ?p" let ?ses_id_t = "param1 ?p_t" let ?time_out = "param2 ?p" let ?time_out_t = "param2 ?p_t" let ?cmd_id = "param6 ?p" let ?cmd_id_t = "param6 ?p_t" let ?in_params = "param7 ?p" let ?in_params_t = "param7 ?p_t" let ?out_params = "param8 ?p" let ?out_params_t = "param8 ?p_t" let ?sesID = "the ?ses_id" let ?sesID_t = "the ?ses_id_t" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?serverID_t = "findSesServTid ?t ?sesID" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?server_tid_t = "the(findSesServTid ?t ?sesID)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServTaState_t = "(TAs_state ?t) (the ?serverID)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?curServSessList_t = "TA_sessions (the ?curServTaState_t)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?isSessIdInSessList_t = "isSessIdInTaInsSessList ?curServSessList_t ?sesID_t" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec_t⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sc ?s_rev_event ?cmd_id ?server_tid" let ?t_invoke = "TA_InvokeCommandEntryPoint sc ?t_rev_event ?cmd_id_t ?server_tid_t" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?t_postOps = "TEE_MgrPostOps ?t_invoke ?server_tid_t" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?post_param_ops_t = "TEE_post_param_operation ?in_params_t" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈" let ?param_error_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sc) (?param_error, TEEC_IC4))" let ?t_error_ret = "setCurDomainAndEvent ?t_rev_event (TEE sc) (?param_error_t, TEEC_IC4)" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈" let ?param_success_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sc) (?param_success, TEEC_IC4))" let ?t_success_ret = "setCurDomainAndEvent ?t_postOps (TEE sc) (?param_success_t, TEEC_IC4)" have a0: "current s=current ?t ∧ TEE_state s =TEE_state ?t ∧ exec_prime s=exec_prime ?t" by simp have a00: "?exec = ?exec_t ∧ ?p = ?p_t ∧ ?ses_id = ?ses_id_t ∧ ?time_out = ?time_out_t ∧ ?cmd_id = ?cmd_id_t ∧ ?in_params = ?in_params_t ∧ ?out_params = ?out_params_t ∧ ?sesID = ?sesID_t ∧ ?serverID = ?serverID_t ∧ ?server_tid = ?server_tid_t ∧ ?isSessIdInSessList = ?isSessIdInSessList_t ∧ ?curServSessList = ?curServSessList_t" by auto have a01: "?t' = ⇑(?s')" proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3") case True have a1: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3" using True by blast have a2: "?t = ?t'" using TEEC_InvokeCommand3_def True a1 a0 by (smt (z3) eq_fst_iff nintf_neq) have a3: "?s' = s" using TEEC_InvokeCommand3R_def True a1 a0 by (smt (z3) eq_fst_iff nintf_neq) then show ?thesis using a2 a3 by simp next case False have a4: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3)" using False by blast have a4_1: "¬(?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current ?t ≠ ?server_tid_t ∨ snd (hd (exec_prime ?t)) ≠ TEEC_IC3)" by (metis a0 a4) then show ?thesis proof(cases "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None") case True have a5: "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None" using True by auto have a5_1: "?ses_id_t = None ∨ ?cmd_id_t = None ∨ ?isSessIdInSessList_t ≠ True ∨ ?serverID_t = None" using a5 a0 a00 by metis have a6: "?s' = ?s_error_ret" using TEEC_InvokeCommand3R_def a5 a4 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a7: "?t' = ?t_error_ret" using TEEC_InvokeCommand3_def a5 a4 a6 a0 a00 a4_1 a5_1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a8: "?t_rev_event = ⇑?s_rev_event" using a5 by simp have a8_0: "?t_invoke = TA_InvokeCommandEntryPoint sc ?t_rev_event ?cmd_id ?server_tid" by auto have a9: "?t_invoke = ⇑?s_invoke" using TA_InvokeCommandEntryPointR_def TA_InvokeCommandEntryPoint_def a8 a8_0 a00 TA_InvokeCommandEntryPoint_refine by presburger have a10: "?t_postOps = ⇑?s_postOps" using a9 abs_rev_lemma by presburger have a11: "?t_error_ret = ⇑?s_error_ret" using a00 a8 abs_rev_lemma by presburger have a12: "?t_error_ret = ?t'" using a7 by auto have a13: "?s_error_ret = ?s'" by (metis a6) then show ?thesis using a11 a12 a13 by presburger next case False have d1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3 ∨ ?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None)" using False a4 by blast have d2: "¬(?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current ?t = TEE sc ∨ current ?t = REE sc ∨ current ?t ≠ ?server_tid_t ∨ snd (hd (exec_prime ?t)) ≠ TEEC_IC3 ∨ ?ses_id_t = None ∨ ?cmd_id_t = None ∨ ?isSessIdInSessList_t ≠ True ∨ ?serverID_t = None)" using a0 d1 by presburger have d3: "?s_success_ret = ?s'" using TEEC_InvokeCommand3R_def d1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have d4: "?t_success_ret = ?t'" using TEEC_InvokeCommand3_def d2 a00 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a8: "?t_rev_event = ⇑?s_rev_event" by simp have a9: "?t_invoke = ⇑?s_invoke" using TA_InvokeCommandEntryPointR_def TA_InvokeCommandEntryPoint_def using TA_InvokeCommandEntryPoint_refine a8 by presburger have a10: "?t_success_ret = ⇑?s_success_ret" using a00 a9 abs_rev_lemma by presburger then show ?thesis using d3 d4 by presburger qed qed } then show ?thesis by simp qed lemma TEEC_InvokeCommand4R_refine: "∀s. fst (TEEC_InvokeCommand4 sc (⇑s)) = ⇑(fst(TEEC_InvokeCommand4R sc s))" proof- { fix s let ?s'="fst(TEEC_InvokeCommand4R sc s)" let ?t = "⇑s" let ?t' = "fst(TEEC_InvokeCommand4 sc ?t)" let ?exec = "(exec_prime s)" let ?exec_t = "(exec_prime ?t)" let ?p = "fst (hd ?exec)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id = "param1 ?p" let ?ses_id_t = "param1 ?p_t" let ?time_out = "param2 ?p" let ?time_out_t = "param2 ?p_t" let ?cmd_id = "param6 ?p" let ?cmd_id_t = "param6 ?p_t" let ?in_params = "param7 ?p" let ?in_params_t = "param7 ?p_t" let ?out_params = "param8 ?p" let ?out_params_t = "param8 ?p_t" let ?teec_ret_code = "param12 ?p" let ?teec_ret_code_t = "param12 ?p_t" let ?tee_ret_code = "param13 ?p" let ?tee_ret_code_t = "param13 ?p_t" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec_t⦈" let ?s_driver_success = "fst(Driver_Write_smc ?s_rev_event zx_mgr ZX_OKr smc_ex_init2)" let ?param_call_closeSession = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = Some ⦇login=DTC_IDENTITY,id=Some 0⦈, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12 = ?teec_ret_code, param13 = ?tee_ret_code⦈" let ?param_call_closeSession_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = Some ⦇login=DTC_IDENTITY,id=Some 0⦈, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12 = ?teec_ret_code_t, param13 = ?tee_ret_code_t⦈" let ?s_call_closeSession = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sc) (?param_call_closeSession, TEEC_CS2))" let ?t_call_closeSession = "setCurDomainAndEvent ?t_rev_event (TEE sc) (?param_call_closeSession_t, TEEC_CS2)" let ?s_driver_error = "fst(Driver_Write_smc ?s_call_closeSession zx_mgr ZX_ERR_INTERNALr smc_ex_init)" have a0: "current s = current ?t ∧ TEE_state s = TEE_state ?t ∧ exec_prime s = exec_prime ?t" by simp have a00: "(exec_prime s) = (exec_prime ?t) ∧ (snd (hd (exec_prime s))) = (snd (hd (exec_prime ?t))) ∧ current s = current ?t ∧ ?teec_ret_code = ?teec_ret_code_t" by simp have a01:"?t' =⇑(?s')" proof- { show ?thesis proof(cases "(exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sc") case True have a1: "(exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sc" using True by auto have a2: "?t = ?t'" using TEEC_InvokeCommand4_def a1 by auto have a3: "s = ?s'" using TEEC_InvokeCommand4R_def a1 by auto then show ?thesis using a2 a3 by simp next case False have a4: "¬((exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sc)" using False by auto have a4_1: "¬((exec_prime ?t) =[] ∨ snd (hd (exec_prime ?t)) ≠ TEEC_IC4 ∨ current ?t ≠ TEE sc)" using False a00 a4 by metis have a5: "?t_rev_event = (⇑?s_rev_event)" by simp have a6: "?t_call_closeSession = ⇑?s_call_closeSession" using a5 abs_rev_lemma using a00 by presburger have a7: "(⇑?s_call_closeSession) = (⇑?s_driver_error)" using Driver_Write_smc_not_change_old Driver_Write_smc_def by simp have a8: "(⇑?s_rev_event) = (⇑?s_driver_success)" using Driver_Write_smc_not_change_old Driver_Write_smc_def by simp show ?thesis proof(cases "?teec_ret_code ≠ (Some TEEC_SUCCESS)") case True have b1: "?teec_ret_code ≠ (Some TEEC_SUCCESS)" by (simp add: True) have b1_1: "?teec_ret_code_t ≠ (Some TEEC_SUCCESS)" using b1 by auto have b2: "?s' = ?s_driver_error" using TEEC_InvokeCommand4R_def a4 b1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis proof- { have b3: "?t' = ?t_call_closeSession" using TEEC_InvokeCommand4_def b1 b2 a4 a0 a00 a4_1 b1_1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) show ?thesis using b2 b3 using a6 a7 by presburger } qed next case False have b4: "¬(?teec_ret_code ≠ (Some TEEC_SUCCESS))" by (simp add: False) have b5: "¬(?teec_ret_code_t ≠ (Some TEEC_SUCCESS))" using b4 by auto then show ?thesis proof- { have b6: "?t' = ?t_rev_event" using b5 TEEC_InvokeCommand4_def a4_1 by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have b7: "?s' = ?s_driver_success" using b5 TEEC_InvokeCommand4R_def a4 TEEC_OpenSession4_def abstract_state_def abstract_state_rev_def Driver_Write_smc_def by simp show ?thesis using b6 b7 by (metis a5 a8) } qed qed qed } qed } then show ?thesis by blast qed subsection "TEE side" lemma TEE_InvokeTACommand1R_refine: "∀s. fst (TEE_InvokeTACommand1 sc (⇑s) memBlock_memRef) = ⇑(fst (TEE_InvokeTACommand1R sc s memBlock_memRef))" using TEE_InvokeTACommand1R_def TEE_InvokeTACommand1_def abstract_state_def abstract_state_rev_def by (smt (z3) State.select_convs(1) State.select_convs(2) State.select_convs(3) State.select_convs(4) State.select_convs(5) State.select_convs(6) State.surjective State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) fstI old.unit.exhaust) lemma TEE_InvokeTACommand2R_refine: "∀s. fst (TEE_InvokeTACommand2 sc (⇑s)) = ⇑(fst (TEE_InvokeTACommand2R sc s))" using TEE_InvokeTACommand2_def TEE_InvokeTACommand2R_def abstract_state_def abstract_state_rev_def by (metis abs_rev_lemma fstI) lemma TEE_InvokeTACommand3R_refine: "∀s. fst (TEE_InvokeTACommand3 sc (⇑s)) = ⇑(fst(TEE_InvokeTACommand3R sc s))" proof- { fix s let ?s' = "fst(TEE_InvokeTACommand3R sc s)" let ?t = "⇑s" let ?t' = "fst(TEE_InvokeTACommand3 sc ?t)" let ?exec = "(exec_prime s)" let ?exec_t = "(exec_prime ?t)" let ?p = "fst (hd ?exec)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id = "param1 ?p" let ?ses_id_t = "param1 ?p_t" let ?time_out = "param2 ?p" let ?time_out_t = "param2 ?p_t" let ?cmd_id = "param6 ?p" let ?cmd_id_t = "param6 ?p_t" let ?in_params = "param7 ?p" let ?in_params_t = "param7 ?p_t" let ?out_params = "param8 ?p" let ?out_params_t = "param8 ?p_t" let ?sesID = "the ?ses_id" let ?sesID_t = "the ?ses_id_t" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?serverID_t = "findSesServTid ?t ?sesID_t" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?server_tid_t = "the(findSesServTid ?t ?sesID_t)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServTaState_t = "(TAs_state ?t) (the ?serverID_t)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?curServSessList_t = "TA_sessions (the ?curServTaState_t)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?isSessIdInSessList_t = "isSessIdInTaInsSessList ?curServSessList_t ?sesID_t" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec_t⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sc ?s_rev_event ?cmd_id ?server_tid" let ?t_invoke = "TA_InvokeCommandEntryPoint sc ?t_rev_event ?cmd_id_t ?server_tid_t" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?t_postOps = "TEE_MgrPostOps ?t_invoke ?server_tid_t" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?post_param_ops_t = "TEE_post_param_operation ?in_params_t" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈" let ?param_error_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sc) (?param_error, TEE_IC4))" let ?t_error_ret = "setCurDomainAndEvent ?t_rev_event (TEE sc) (?param_error_t, TEE_IC4)" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈" let ?param_success_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sc) (?param_success, TEE_IC4))" let ?t_success_ret = "setCurDomainAndEvent ?t_postOps (TEE sc) (?param_success_t, TEE_IC4)" have a0: "current s=current ?t ∧ TEE_state s =TEE_state ?t ∧ exec_prime s=exec_prime ?t" by simp have a00: "?exec = ?exec_t ∧ ?p = ?p_t ∧ ?ses_id = ?ses_id_t ∧ ?time_out = ?time_out_t ∧ ?cmd_id = ?cmd_id_t ∧ ?in_params = ?in_params_t ∧ ?out_params = ?out_params_t ∧ ?sesID = ?sesID_t ∧ ?serverID = ?serverID_t ∧ ?server_tid = ?server_tid_t ∧ ?isSessIdInSessList = ?isSessIdInSessList_t ∧ ?curServSessList = ?curServSessList_t" by auto have a01: "?t' = ⇑(?s')" proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3") case True have a1: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3" using True by auto have a1_1: "?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current ?t = TEE sc ∨ current ?t = REE sc ∨ current ?t ≠ ?server_tid_t ∨ snd (hd (exec_prime ?t)) ≠ TEE_IC3" using a0 a1 by presburger have a2: "?t = ?t'" using TEE_InvokeTACommand3_def True a1 a0 by (smt (z3) eq_fst_iff nintf_neq) have a3: "?s' = s" using TEE_InvokeTACommand3R_def True a1 a0 by (smt (z3) eq_fst_iff nintf_neq) then show ?thesis using a2 by auto next case False have a4: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3)" using False by blast have a4_1: "¬(?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current ?t = TEE sc ∨ current ?t = REE sc ∨ current ?t ≠ ?server_tid_t ∨ snd (hd (exec_prime ?t)) ≠ TEE_IC3)" using a4 by auto then show ?thesis proof(cases "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None") case True have a5: "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None" using True by auto have a5_1: "?ses_id_t = None ∨ ?cmd_id_t = None ∨ ?isSessIdInSessList_t ≠ True ∨ ?serverID_t = None" using a5 a0 a00 by metis have a6: "?s' = ?s_error_ret" using TEE_InvokeTACommand3R_def a5 a4 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a7: "?t' = ?t_error_ret" using TEE_InvokeTACommand3_def a5 a4 a6 a0 a00 a4_1 a5_1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a8: "?t_rev_event = ⇑?s_rev_event" using a5 by simp have a8_0: "?t_invoke = TA_InvokeCommandEntryPoint sc ?t_rev_event ?cmd_id ?server_tid" by auto have a9: "?t_invoke = ⇑?s_invoke" using TA_InvokeCommandEntryPointR_def TA_InvokeCommandEntryPoint_def a8 a8_0 a00 TA_InvokeCommandEntryPoint_refine by presburger have a10: "?t_postOps = ⇑?s_postOps" using a9 abs_rev_lemma using a00 by presburger have a11: "?t_error_ret = ⇑?s_error_ret" using a00 a8 abs_rev_lemma by presburger have a12: "?t_error_ret = ?t'" using a7 by auto have a13: "?s_error_ret = ?s'" by (metis a6) then show ?thesis using a11 a12 a13 by presburger next case False have d1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sc ∨ current s = REE sc ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3 ∨ ?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None)" using False a4 by blast have d2: "¬(?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current ?t = TEE sc ∨ current ?t = REE sc ∨ current ?t ≠ ?server_tid_t ∨ snd (hd (exec_prime ?t)) ≠ TEE_IC3 ∨ ?ses_id_t = None ∨ ?cmd_id_t = None ∨ ?isSessIdInSessList_t ≠ True ∨ ?serverID_t = None)" using a0 d1 by presburger have d3: "?s_success_ret = ?s'" using TEE_InvokeTACommand3R_def d1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have d4: "?t_success_ret = ?t'" using TEE_InvokeTACommand3_def d2 a00 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) have a8: "?t_rev_event = ⇑?s_rev_event" by simp have a9: "?t_invoke = ⇑?s_invoke" using TA_InvokeCommandEntryPointR_def TA_InvokeCommandEntryPoint_def using TA_InvokeCommandEntryPoint_refine a8 by presburger have a10: "?t_success_ret = ⇑?s_success_ret" using a00 a9 abs_rev_lemma by presburger then show ?thesis using d3 d4 by presburger qed qed } then show ?thesis by simp qed lemma TEE_InvokeTACommand4R_refine: "∀s. fst (TEE_InvokeTACommand4 sc (⇑s)) = ⇑(fst(TEE_InvokeTACommand4R sc s))" using TEE_InvokeTACommand4_def TEE_InvokeTACommand4R_def abstract_state_def abstract_state_rev_def by (metis abs_rev_lemma fstI) section "security proof" subsection "TEEC side" subsubsection "TEEC_InvokeCommand1R" lemma TEEC_InvokeCommand1R_notchnew: assumes p1: "s'=(fst (TEEC_InvokeCommand1R sc s ses_id time_out cmd_id in_params out_params memBlock_memRef))" shows "(s ∼. d .∼Δ s')" using TEEC_InvokeCommand1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEEC_InvokeCommand1R_integrity: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND1 ses_id time_out cmd_id in_params out_params memBlock_memRef)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1: "s' = fst (TEEC_InvokeCommand1R sysconf s ses_id time_out cmd_id in_params out_params memBlock_memRef)" using exec_eventR_def a3 p1 by simp have b2: "(s ∼. d .∼Δ s')" using TEEC_InvokeCommand1R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEEC_InvokeCommand1R_integrity_e: "integrity_new_e (hyperc' (TEEC_INVOKECOMMAND1 ses_id time_out cmd_id in_params out_params memBlock_memRef))" using TEEC_InvokeCommand1R_integrity integrity_new_e_def by metis lemma TEEC_InvokeCommand1R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND1 ses_id time_out cmd_id in_params out_params memBlock_memRef)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'= fst (TEEC_InvokeCommand1R sysconf s ses_id time_out cmd_id in_params out_params memBlock_memRef)" using exec_eventR_def a7 p1 by simp have b2:"t'= fst (TEEC_InvokeCommand1R sysconf t ses_id time_out cmd_id in_params out_params memBlock_memRef)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEEC_InvokeCommand1R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEEC_InvokeCommand1R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_INVOKECOMMAND1 ses_id time_out cmd_id in_params out_params memBlock_memRef))" using TEEC_InvokeCommand1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEEC_InvokeCommand2R" lemma TEEC_InvokeCommand2R_integrity: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND2)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "tee_invokeTACommand_TEEDomain2R sysconf ?s_rev_event ?ses_id ?time_out ?cmd_id ?in_params ?out_params" let ?s_state = "fst ?s_invoke" let ?s2 = "Driver_Read ?s_state smc_ex_init_read zx_mgr" let ?s_origin = "fst(snd ?s_invoke)" let ?s_code = "fst(snd (snd ?s_invoke))" let ?s_params = "(snd (snd (snd ?s_invoke)))" have a4: "exec_eventR a = {(s,s'). s'∈{fst (TEEC_InvokeCommand2R sysconf s)}}" using p1 exec_eventR_def by auto have a41: "s' = fst (TEEC_InvokeCommand2R sysconf s)" using a3 a4 by auto have a5: "s≠s'⟶((the (domain_of_eventR s a)) ∖↝ (TEE sysconf))" by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def) have a6: "?domain ≠d" using a2 nintf_neq by blast have a7: "?domain = (current s)" using domain_of_eventR_def using p1 by auto have "(s ∼. d .∼Δ s')" proof(cases "current s ≠ TEE sysconf ∨ (exec_prime s) = [] ∨ (snd (hd (exec_prime s)) ≠ TEEC_IC2)") case True have "s = s'" using TEEC_InvokeCommand2R_def a41 by (smt (z3) a5 a7 eq_fst_iff nintf_neq) then show ?thesis using vpeq_ipc_reflexive_lemma by blast next case False have b1: "¬(current s ≠ TEE sysconf ∨ (exec_prime s) = [] ∨ (snd (hd (exec_prime s)) ≠ TEEC_IC2))" using False by auto then show ?thesis proof(cases "d = REE sysconf") case True then have b2:"(s ∼. d .∼Δ s') = True" using tee_no_ree vpeq_ipc_def by auto then show ?thesis by auto next case False have b4:"d≠REE sysconf" by (simp add: False) then show ?thesis proof(cases "d=TEE sysconf") case True have b5:"d=TEE sysconf" by (simp add: True) have b7:"(s ∼. d .∼Δ s')" proof- { have c1:"TEE_state ?s_rev_event =TEE_state s" by simp have c2:"vpeq_ipc ?s_rev_event (TEE sysconf) ?s_state" using a6 a7 b1 b5 by auto have c4:"vpeq_ipc ?s2 (TEE sysconf) ?s_state" using a6 a7 b1 b5 by auto then show ?thesis using a6 a7 b1 by auto } qed then show ?thesis by auto next case False have b8:"is_TA sysconf d" using False b4 by auto have b9:"(s ∼. d .∼Δ s') = True" by (meson False ins_no_intf_tee interference1_def vpeq_ipc_def) then show ?thesis by auto qed qed qed } then show ?thesis by blast qed lemma TEEC_InvokeCommand2R_integrity_e: "integrity_new_e (hyperc' (TEEC_INVOKECOMMAND2))" using TEEC_InvokeCommand2R_integrity integrity_new_e_def by metis lemma TEEC_InvokeCommand2R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND2)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t)∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "tee_invokeTACommand_TEEDomain2R sysconf ?s_rev_event ?ses_id ?time_out ?cmd_id ?in_params ?out_params" let ?s_state = "fst ?s_invoke" let ?s2 = "Driver_Read ?s_state smc_ex_init_read zx_mgr" let ?s_origin = "fst(snd ?s_invoke)" let ?s_code = "fst(snd (snd ?s_invoke))" let ?s_params = "(snd (snd (snd ?s_invoke)))" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?time_out_t = "param2 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?sesID_t = "the ?ses_id_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?t_invoke = "tee_invokeTACommand_TEEDomain2R sysconf ?t_rev_event ?ses_id_t ?time_out_t ?cmd_id_t ?in_params_t ?out_params_t" let ?t_state = "fst ?t_invoke" let ?t2 = "Driver_Read ?t_state smc_ex_init_read zx_mgr" let ?t_origin = "fst(snd ?t_invoke)" let ?t_code = "fst(snd (snd ?t_invoke))" let ?t_params = "(snd (snd (snd ?t_invoke)))" have "(s' ∼. d .∼Δ t')" proof- { have b1: "s' = fst (TEEC_InvokeCommand2R sysconf s)" using exec_eventR_def p1 a7 by simp have b2: "t' = fst (TEEC_InvokeCommand2R sysconf t)" using exec_eventR_def p1 a8 by simp have b3: "current s=current t" using domain_of_eventR_def a4 by simp have b4: "?exec = ?exec_t" by (simp add: a31) show ?thesis proof(cases "current s ≠ TEE sysconf ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC2") case True have c1: "current s ≠ TEE sysconf ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC2" using True by auto have c2: "s' = s" using c1 b1 TEEC_InvokeCommand2R_def by (smt (z3) prod.collapse prod.inject) have c3: "t' = t" using c1 b2 TEEC_InvokeCommand2R_def by (smt (z3) a31 b3 prod.collapse prod.inject) then show ?thesis using a3 c2 vpeqR_def by blast next case False have c4: "¬(current s ≠ TEE sysconf ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC2)" using False by auto have c4_1: "¬(current t ≠ TEE sysconf ∨ (exec_prime t) = [] ∨ snd (hd (exec_prime t)) ≠ TEEC_IC2)" using b3 b4 c4 by auto have c5: "is_TEE sysconf (current s)" using is_TEE_def c4 by auto then show ?thesis proof(cases "d = TEE sysconf") case True have c6: "is_TEE sysconf d = True" using True is_TEE_def by blast have d1: "vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by auto have d2: "vpeq_ipc ?s_state d ?t_state" using d1 tee_invokeTACommand_TEEDomain2R_notchnew by (smt (verit) vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) have d3: "vpeq_ipc ?s2 d ?t2" using Driver_Read_def d2 by simp have d4: "?s2 = s'" using c4 TEEC_InvokeCommand2R_def b1 fst_conv by (smt (z3) False State.unfold_congs(1) State.unfold_congs(6) fst_conv) have d5: "?t2 = t'" using c4_1 TEEC_InvokeCommand2R_def b2 fst_conv by (smt (z3) False State.unfold_congs(1) State.unfold_congs(6) fst_conv) then show ?thesis using d3 d4 by blast next case False have c7: "d ≠ TEE sysconf" by (simp add: False) then show ?thesis proof(cases "d = REE sysconf") case True then show ?thesis using is_TEE_def vpeq_ipc_def c7 by auto next case False have c8: "is_TA sysconf d" using is_TA_def False c7 by auto have c9:"(s' ∼. d .∼Δ t') = True" using c7 by auto then show ?thesis by auto qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) Pair_inject) qed lemma TEEC_InvokeCommand2R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_INVOKECOMMAND2))" using TEEC_InvokeCommand2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEEC_InvokeCommand3R" lemma TEEC_InvokeCommand3R_integrity: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND3)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sysconf ?s_rev_event ?cmd_id ?server_tid" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sysconf) (?param_error, TEEC_IC4))" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sysconf) (?param_success, TEEC_IC4))" have a4: "exec_eventR a = {(s,s'). s'∈{fst (TEEC_InvokeCommand3R sysconf s)}}" using p1 exec_eventR_def by auto have a41: "s' = fst (TEEC_InvokeCommand3R sysconf s)" using a3 a4 by auto have a5: "s≠s'⟶((the (domain_of_eventR s a)) ∖↝ (TEE sysconf))" by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def) have a6: "?domain ≠d" using a2 nintf_neq by blast have a7: "?domain = (current s)" using domain_of_eventR_def using p1 by auto have "(s ∼. d .∼Δ s')" proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3") case True have b0: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3" using True by auto have "s = s'" using TEEC_InvokeCommand3R_def a41 b0 by (smt (z3) eq_fst_iff nintf_neq) then show ?thesis using vpeq_ipc_reflexive_lemma by blast next case False have b1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3)" using False by blast then show ?thesis proof(cases "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None") case True have b2: "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None" using True by auto have b3: "s' = ?s_error_ret" using TEEC_InvokeCommand3R_def b1 b2 a41 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis proof(cases "d = REE sysconf") case True have b4: "(s ∼. d .∼Δ s') = True" using tee_no_ree vpeq_ipc_def using True by auto then show ?thesis by blast next case False have b4:"d ≠ REE sysconf" by (simp add: False) then show ?thesis proof(cases "d = TEE sysconf") case True have b5: "d = TEE sysconf" by (simp add: True) have b7: "(s ∼. d .∼Δ s')" proof- { have c1: "TEE_state ?s_rev_event =TEE_state s" by simp have c2: "vpeq_ipc ?s_rev_event (TEE sysconf) ?s_invoke" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TA_InvokeCommandEntryPointR_def by auto have c3: "vpeq_ipc ?s_invoke (TEE sysconf) ?s_postOps" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TEE_MgrPostOps_def by simp have c4: "vpeq_ipc ?s_postOps (TEE sysconf) ?s_error_ret" using abstract_state_def abstract_state_rev_def vpeq_ipc_def setCurDomainAndEvent_def c2 by auto then show ?thesis using c4 b3 by simp } qed then show ?thesis by blast next case False have b8: "is_TA sysconf d" by (metis False b4 is_TA_def) have b9: "(s ∼. d .∼Δ s') = True" using False by auto then show ?thesis by blast qed qed next case False have d1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3 ∨ ?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None)" using False b1 by blast have d2: "s' = ?s_success_ret" using TEEC_InvokeCommand3R_def d1 a41 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis proof(cases "d = REE sysconf") case True have d3:"(s ∼. d .∼Δ s') = True" using tee_no_ree vpeq_ipc_def True by auto then show ?thesis by blast next case False have d4:"d ≠ REE sysconf" by (simp add: False) then show ?thesis proof(cases "d = TEE sysconf") case True have d5: "d = TEE sysconf" by (simp add: True) have d6: "(s ∼. d .∼Δ s')" proof- { have e1: "TEE_state ?s_rev_event = TEE_state s" by simp have e1_0: "vpeq_ipc s (TEE sysconf) ?s_rev_event" using abstract_state_def abstract_state_rev_def vpeq_ipc_def by simp have e2: "vpeq_ipc ?s_rev_event (TEE sysconf) ?s_invoke" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TA_InvokeCommandEntryPointR_def by auto have e3: "vpeq_ipc ?s_invoke (TEE sysconf) ?s_postOps" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TEE_MgrPostOps_def by simp have e4: "vpeq_ipc ?s_postOps (TEE sysconf) ?s_success_ret" using abstract_state_def abstract_state_rev_def vpeq_ipc_def setCurDomainAndEvent_def by simp have e5: "s' = ?s_success_ret" by (simp add: d2) then show ?thesis using e1 e1_0 e2 e3 e4 e5 vpeq_ipc_def using d5 by auto } qed then show ?thesis by blast next case False have d8: "is_TA sysconf d" using False d4 by auto have d9: "(s ∼. d .∼Δ s') = True" using False by auto then show ?thesis by blast qed qed qed qed } then show ?thesis by blast qed lemma TEEC_InvokeCommand3R_integrity_e: "integrity_new_e (hyperc' (TEEC_INVOKECOMMAND3))" using TEEC_InvokeCommand3R_integrity integrity_new_e_def by metis lemma TEEC_InvokeCommand3R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND3)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t)∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a51: "ta_mgr(TEE_state s) =ta_mgr(TEE_state t)" assume a52: "TAs_state s =TAs_state t " assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sysconf ?s_rev_event ?cmd_id ?server_tid" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sysconf) (?param_error, TEEC_IC4))" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sysconf) (?param_success, TEEC_IC4))" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?time_out_t = "param2 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?sesID_t = "the ?ses_id_t" let ?serverID_t = "findSesServTid (⇑t) ?sesID_t" let ?server_tid_t = "the(findSesServTid (⇑t) ?sesID_t)" let ?curServTaState_t = "(TAs_state (⇑t)) (the ?serverID_t)" let ?curServSessList_t = "TA_sessions (the ?curServTaState_t)" let ?isSessIdInSessList_t = "isSessIdInTaInsSessList ?curServSessList_t ?sesID_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?t_invoke = "TA_InvokeCommandEntryPointR sysconf ?t_rev_event ?cmd_id_t ?server_tid_t" let ?t_postOps = "?t_invoke⇓(TEE_MgrPostOps (⇑?t_invoke) ?server_tid_t)" let ?post_param_ops_t = "TEE_post_param_operation ?in_params_t" let ?param_error_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=Some TEEC_ERROR_BAD_PARAMETERS, param13=None⦈" let ?t_error_ret = "?t_rev_event⇓(setCurDomainAndEvent (⇑?t_rev_event) (TEE sysconf) (?param_error_t, TEEC_IC4))" let ?param_success_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=Some TEEC_SUCCESS, param13=None⦈" let ?t_success_ret = "?t_postOps⇓(setCurDomainAndEvent (⇑?t_postOps) (TEE sysconf) (?param_success_t, TEEC_IC4))" have a10: "s' = fst (TEEC_InvokeCommand3R sysconf s)" using exec_eventR_def p1 a7 by simp have a11: "t' = fst (TEEC_InvokeCommand3R sysconf t)" using exec_eventR_def p1 a8 by simp have a12: "current s = current t" using domain_of_eventR_def a4 by auto have a13: "ta_mgr(TEE_state s) = ta_mgr(TEE_state t)" using a3 vpeq1_def a51 by auto have a14: "?sesID = ?sesID_t" by (simp add: a31) have a15: "?serverID = ?serverID_t" using mgr_ta_sessions_findSesServTid a14 a51 abstract_state_def by simp have a16: "?ses_id = ?ses_id_t" by (simp add: a31) have a17: "?cmd_id = ?cmd_id_t" by (simp add: a31) have a18: "?isSessIdInSessList = ?isSessIdInSessList_t" using isSessIdInTaInsSessList_def a52 using a15 a31 by auto have "(s' ∼. d .∼Δ t')" proof- { have b1: "s' = fst(TEEC_InvokeCommand3R sysconf s)" using exec_eventR_def p1 a7 by simp have b2: "t' = fst(TEEC_InvokeCommand3R sysconf t)" using exec_eventR_def p1 a8 by simp have b3: "current s = current t" using domain_of_eventR_def a4 by simp have b4: "?exec = ?exec_t" by (simp add: a31) show ?thesis proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3") case True have c1: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3" by (meson True) have c1_1: "?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current t = TEE sysconf ∨ current t = REE sysconf ∨ current t ≠ ?server_tid_t ∨ snd (hd (exec_prime t)) ≠ TEEC_IC3" using a15 b3 b4 c1 by auto have c2: "s' = s" using c1 b1 TEEC_InvokeCommand3R_def by (smt (z3) prod.collapse prod.inject) have c3: "t' = t" using c1 b2 b3 b4 TEEC_InvokeCommand3R_def a31 c1_1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis using a3 c2 vpeqR_def by blast next case False have c4: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEEC_IC3)" using False by auto have c5: "is_TA sysconf (current s)" using is_TA_def by (metis c4) then show ?thesis proof(cases "d = TEE sysconf") case True then show ?thesis using a5 c5 domain_of_eventR_def by force next case False have c6:"d ≠ TEE sysconf" by (simp add: False) then show ?thesis proof(cases "d = REE sysconf") case True then show ?thesis using a5 c5 using domain_of_eventR_def by force next case False have c7:"is_TA sysconf d" using is_TA_def c6 using False by auto have c8:"(s' ∼. d .∼Δ t') =True" using c6 is_TEE_def vpeq_ipc_def by presburger then show ?thesis by auto qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) Pair_inject) qed lemma TEEC_InvokeCommand3R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_INVOKECOMMAND3))" using TEEC_InvokeCommand3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEEC_InvokeCommand4R" lemma TEEC_InvokeCommand4R_integrity: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND4)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?exec = "exec_prime s" let ?p = "fst (hd (?exec))" have a4:"s'=fst(TEEC_InvokeCommand4R sysconf s)" using exec_eventR_def a3 p1 by simp have "(s ∼. d .∼Δ s')" proof(cases "(exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sysconf") case True then show ?thesis using TEEC_InvokeCommand4R_def a4 by fastforce next case False have b0: "¬((exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sysconf)" using False by auto then show ?thesis proof(cases "d = TEE sysconf") case True then show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by simp next case False have b4: "d ≠ TEE sysconf" using False by simp then show ?thesis proof(cases "d = REE sysconf") case True then show ?thesis using True a2 interference1_def b0 domain_of_eventR_def by auto next case False have b5:"d ≠ REE sysconf" by (simp add: False) have b6:"is_TA sysconf d" using b4 b5 by auto then show ?thesis using b6 a2 interference1_def by simp qed qed qed } thus ?thesis using vpeq_transitive_lemma by blast qed lemma TEEC_InvokeCommand4R_integrity_e: "integrity_new_e (hyperc' (TEEC_INVOKECOMMAND4))" using TEEC_InvokeCommand4R_integrity integrity_new_e_def by metis lemma TEEC_InvokeCommand4R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_INVOKECOMMAND4)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t)∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?teec_ret_code = "param12 ?p" let ?tee_ret_code = "param13 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_driver_success = "fst(Driver_Write_smc ?s_rev_event zx_mgr ZX_OKr smc_ex_init2)" let ?param_call_closeSession = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = Some ⦇login=DTC_IDENTITY,id=Some 0⦈, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=?teec_ret_code, param13=?tee_ret_code⦈" let ?s_call_closeSession = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sysconf) (?param_call_closeSession, TEEC_CS2))" let ?s_driver_error = "fst(Driver_Write_smc ?s_call_closeSession zx_mgr ZX_ERR_INTERNALr smc_ex_init)" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?time_out_t = "param2 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?teec_ret_code_t = "param12 ?p_t" let ?tee_ret_code_t = "param13 ?p_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?t_driver_success = "fst(Driver_Write_smc ?t_rev_event zx_mgr ZX_OKr smc_ex_init2)" let ?param_call_closeSession_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = Some ⦇login=DTC_IDENTITY,id=Some 0⦈, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=?teec_ret_code_t, param13=?tee_ret_code_t⦈" let ?t_call_closeSession = "?t_rev_event⇓(setCurDomainAndEvent (⇑?t_rev_event) (TEE sysconf) (?param_call_closeSession_t, TEEC_CS2))" let ?t_driver_error = "fst(Driver_Write_smc ?t_call_closeSession zx_mgr ZX_ERR_INTERNALr smc_ex_init)" have a0: "exec_prime s = exec_prime t ∧ (snd (hd (exec_prime s))) = (snd (hd (exec_prime t))) ∧ current s = current t ∧ ?teec_ret_code = ?teec_ret_code_t" using a31 a4 domain_of_eventR_def by auto have "(s' ∼. d .∼Δ t')" proof- { have b1: "s' = fst(TEEC_InvokeCommand4R sysconf s)" using exec_eventR_def p1 a7 by simp have b2: "t'=fst(TEEC_InvokeCommand4R sysconf t)" using exec_eventR_def p1 a8 by simp have b3: "current s=current t" using domain_of_eventR_def a4 by simp show ?thesis proof(cases "(exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sysconf") case True have c1: "(exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sysconf" using True by blast have c2: "(exec_prime t) =[] ∨ snd (hd (exec_prime t)) ≠ TEEC_IC4 ∨ current t ≠ TEE sysconf" using a0 c1 by auto have c3: "s' = s" using c1 b1 TEEC_InvokeCommand4R_def by auto have c4: "t' = t" using c2 b2 TEEC_InvokeCommand4R_def by auto then show ?thesis by (metis a3 c3 vpeqR_def) next case False have c5: "¬((exec_prime s) =[] ∨ snd (hd (exec_prime s)) ≠ TEEC_IC4 ∨ current s ≠ TEE sysconf)" using False by auto have c6: "¬((exec_prime t) =[] ∨ snd (hd (exec_prime t)) ≠ TEEC_IC4 ∨ current t ≠ TEE sysconf)" using a0 c5 by auto have d1: "vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by auto have d2: "vpeq_ipc ?s_driver_success d ?t_driver_success" using d1 a3 Driver_Write_smc_def by auto have d3: "vpeq_ipc ?s_call_closeSession d ?t_call_closeSession" using d2 a3 setCurDomainAndEvent_def by auto have d4: "vpeq_ipc ?s_driver_error d ?t_driver_error" using d3 Driver_Write_smc_def a3 by auto then show ?thesis proof(cases "?teec_ret_code ≠ (Some TEEC_SUCCESS)") case True have c7: "?teec_ret_code ≠ (Some TEEC_SUCCESS)" by (simp add: True) have c8: "?teec_ret_code_t ≠ (Some TEEC_SUCCESS)" using a0 c7 by auto have c9: "s' = ?s_driver_error" using c7 c5 b1 TEEC_InvokeCommand4R_def by (smt (verit, best) State.fold_congs(6) fst_conv) have c10: "t' = ?t_driver_error" using c8 c6 b2 TEEC_InvokeCommand4R_def by (smt (verit, best) State.fold_congs(6) fst_conv) then show ?thesis using c9 c10 d4 by blast next case False have c11: "¬(?teec_ret_code ≠ (Some TEEC_SUCCESS))" by (simp add: False) have c11_1: "¬(?teec_ret_code_t ≠ (Some TEEC_SUCCESS))" using a0 c11 by auto then show ?thesis proof- { have c10: "s' = ?s_driver_success" using b1 c11 c5 TEEC_InvokeCommand4R_def by (smt (verit, best) State.fold_congs(6) fst_conv) have c11: "t' = ?t_driver_success" using b2 c11_1 c6 TEEC_InvokeCommand4R_def by (smt (verit, best) State.fold_congs(6) fst_conv) show ?thesis using c10 c11 d2 by argo } qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) Pair_inject) qed lemma TEEC_InvokeCommand4R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_INVOKECOMMAND4))" using TEEC_InvokeCommand4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsection "TEE side" subsubsection "TEE_InvokeTACommand1R" lemma TEE_InvokeTACommand1R_integrity: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND1 memBlock_memRef)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1: "s' = fst (TEE_InvokeTACommand1R sysconf s memBlock_memRef)" using exec_eventR_def a3 p1 by simp have b2: "(s ∼. d .∼Δ s')" using TEE_InvokeTACommand1R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_InvokeTACommand1R_integrity_e: "integrity_new_e (hyperc' (TEE_INVOKETACOMMAND1 memBlock_memRef))" using TEE_InvokeTACommand1R_integrity integrity_new_e_def by metis lemma TEE_InvokeTACommand1R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND1 memBlock_memRef)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_InvokeTACommand1R sysconf s memBlock_memRef)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_InvokeTACommand1R sysconf t memBlock_memRef)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_InvokeTACommand1R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_InvokeTACommand1R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_INVOKETACOMMAND1 memBlock_memRef))" using TEE_InvokeTACommand1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEE_InvokeTACommand2R" lemma TEE_InvokeTACommand2R_integrity: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND2)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst (TEE_InvokeTACommand2R sysconf s)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEE_InvokeTACommand2R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_InvokeTACommand2R_integrity_e: "integrity_new_e (hyperc' (TEE_INVOKETACOMMAND2))" using TEE_InvokeTACommand2R_integrity integrity_new_e_def by metis lemma TEE_InvokeTACommand2R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND2)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_InvokeTACommand2R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_InvokeTACommand2R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_InvokeTACommand2R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_InvokeTACommand2R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_INVOKETACOMMAND2))" using TEE_InvokeTACommand2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEE_InvokeTACommand3R" lemma TEE_InvokeTACommand3R_integrity: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND3)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sysconf ?s_rev_event ?cmd_id ?server_tid" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sysconf) (?param_error, TEE_IC4))" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sysconf) (?param_success, TEE_IC4))" have a4: "exec_eventR a = {(s,s'). s'∈{fst (TEE_InvokeTACommand3R sysconf s)}}" using p1 exec_eventR_def by auto have a41: "s' = fst (TEE_InvokeTACommand3R sysconf s)" using a3 a4 by auto have a5: "s≠s'⟶((the (domain_of_eventR s a)) ∖↝ (TEE sysconf))" by (metis a2 ins_no_intf_tee ins_tee_intf_all non_interference1_def) have a6: "?domain ≠d" using a2 nintf_neq by blast have a7: "?domain = (current s)" using domain_of_eventR_def using p1 by auto have "(s ∼. d .∼Δ s')" proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3") case True have b0: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3" using True by auto have "s = s'" using TEE_InvokeTACommand3R_def a41 b0 by (smt (z3) eq_fst_iff nintf_neq) then show ?thesis using vpeq_ipc_reflexive_lemma by blast next case False have b1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3)" using False by blast then show ?thesis proof(cases "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None") case True have b2: "?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None" using True by auto have b3: "s' = ?s_error_ret" using TEE_InvokeTACommand3R_def b1 b2 a41 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis proof(cases "d = REE sysconf") case True have b4: "(s ∼. d .∼Δ s') = True" using tee_no_ree vpeq_ipc_def using True by auto then show ?thesis by blast next case False have b4:"d ≠ REE sysconf" by (simp add: False) then show ?thesis proof(cases "d = TEE sysconf") case True have b5: "d = TEE sysconf" by (simp add: True) have b7: "(s ∼. d .∼Δ s')" proof- { have c1: "TEE_state ?s_rev_event =TEE_state s" by simp have c2: "vpeq_ipc ?s_rev_event (TEE sysconf) ?s_invoke" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TA_InvokeCommandEntryPointR_def by auto have c3: "vpeq_ipc ?s_invoke (TEE sysconf) ?s_postOps" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TEE_MgrPostOps_def by simp have c4: "vpeq_ipc ?s_postOps (TEE sysconf) ?s_error_ret" using abstract_state_def abstract_state_rev_def vpeq_ipc_def setCurDomainAndEvent_def c2 by auto then show ?thesis using c4 b3 by simp } qed then show ?thesis by blast next case False have b8: "is_TA sysconf d" by (metis False b4 is_TA_def) have b9: "(s ∼. d .∼Δ s') = True" using False by auto then show ?thesis by blast qed qed next case False have d1: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3 ∨ ?ses_id = None ∨ ?cmd_id = None ∨ ?isSessIdInSessList ≠ True ∨ ?serverID = None)" using False b1 by blast have d2: "s' = ?s_success_ret" using TEE_InvokeTACommand3R_def d1 a41 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis proof(cases "d = REE sysconf") case True have d3:"(s ∼. d .∼Δ s') = True" using tee_no_ree vpeq_ipc_def True by auto then show ?thesis by blast next case False have d4:"d ≠ REE sysconf" by (simp add: False) then show ?thesis proof(cases "d = TEE sysconf") case True have d5: "d = TEE sysconf" by (simp add: True) have d6: "(s ∼. d .∼Δ s')" proof- { have e1: "TEE_state ?s_rev_event = TEE_state s" by simp have e1_0: "vpeq_ipc s (TEE sysconf) ?s_rev_event" using abstract_state_def abstract_state_rev_def vpeq_ipc_def by simp have e2: "vpeq_ipc ?s_rev_event (TEE sysconf) ?s_invoke" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TA_InvokeCommandEntryPointR_def by auto have e3: "vpeq_ipc ?s_invoke (TEE sysconf) ?s_postOps" using abstract_state_def abstract_state_rev_def vpeq_ipc_def TEE_MgrPostOps_def by simp have e4: "vpeq_ipc ?s_postOps (TEE sysconf) ?s_success_ret" using abstract_state_def abstract_state_rev_def vpeq_ipc_def setCurDomainAndEvent_def by simp have e5: "s' = ?s_success_ret" by (simp add: d2) then show ?thesis using e1 e1_0 e2 e3 e4 e5 vpeq_ipc_def using d5 by auto } qed then show ?thesis by blast next case False have d8: "is_TA sysconf d" using False d4 by auto have d9: "(s ∼. d .∼Δ s') = True" using False by auto then show ?thesis by blast qed qed qed qed } then show ?thesis by blast qed lemma TEE_InvokeTACommand3R_integrity_e: "integrity_new_e (hyperc' (TEE_INVOKETACOMMAND3))" using TEE_InvokeTACommand3R_integrity integrity_new_e_def by metis lemma TEE_InvokeTACommand3R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND3)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t)∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a51: "ta_mgr(TEE_state s) =ta_mgr(TEE_state t)" assume a52: "TAs_state s =TAs_state t " assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?time_out = "param2 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?sesID = "the ?ses_id" let ?serverID = "findSesServTid (⇑s) ?sesID" let ?server_tid = "the(findSesServTid (⇑s) ?sesID)" let ?curServTaState = "(TAs_state (⇑s)) (the ?serverID)" let ?curServSessList = "TA_sessions (the ?curServTaState)" let ?isSessIdInSessList = "isSessIdInTaInsSessList ?curServSessList ?sesID" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_invoke = "TA_InvokeCommandEntryPointR sysconf ?s_rev_event ?cmd_id ?server_tid" let ?s_postOps = "?s_invoke⇓(TEE_MgrPostOps (⇑?s_invoke) ?server_tid)" let ?post_param_ops = "TEE_post_param_operation ?in_params" let ?param_error = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈" let ?s_error_ret = "?s_rev_event⇓(setCurDomainAndEvent (⇑?s_rev_event) (TEE sysconf) (?param_error, TEE_IC4))" let ?param_success = "⦇param1 = ?ses_id, param2 = ?time_out, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id, param7 = ?in_params, param8 = ?out_params, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈" let ?s_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?s_postOps) (TEE sysconf) (?param_success, TEE_IC4))" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?time_out_t = "param2 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?sesID_t = "the ?ses_id_t" let ?serverID_t = "findSesServTid (⇑t) ?sesID_t" let ?server_tid_t = "the(findSesServTid (⇑t) ?sesID_t)" let ?curServTaState_t = "(TAs_state (⇑t)) (the ?serverID_t)" let ?curServSessList_t = "TA_sessions (the ?curServTaState_t)" let ?isSessIdInSessList_t = "isSessIdInTaInsSessList ?curServSessList_t ?sesID_t" let ?t_rev_event = "s⦇exec_prime := tl ?exec_t⦈" let ?t_invoke = "TA_InvokeCommandEntryPointR sysconf ?t_rev_event ?cmd_id_t ?server_tid_t" let ?t_postOps = "?t_invoke⇓(TEE_MgrPostOps (⇑?t_invoke) ?server_tid_t)" let ?post_param_ops_t = "TEE_post_param_operation ?in_params_t" let ?param_error_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_ERROR_BAD_PARAMETERS⦈" let ?t_error_ret = "?t_rev_event⇓(setCurDomainAndEvent (⇑?t_rev_event) (TEE sysconf) (?param_error_t, TEE_IC4))" let ?param_success_t = "⦇param1 = ?ses_id_t, param2 = ?time_out_t, param3 = None, param4 = None, param5 = None, param6 = ?cmd_id_t, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10 = None, param11 = None, param12=None, param13=Some TEE_SUCCESS⦈" let ?t_success_ret = "?s_postOps⇓(setCurDomainAndEvent (⇑?t_postOps) (TEE sysconf) (?param_success_t, TEE_IC4))" have a10: "s' = fst (TEE_InvokeTACommand3R sysconf s)" using exec_eventR_def p1 a7 by simp have a11: "t' = fst (TEE_InvokeTACommand3R sysconf t)" using exec_eventR_def p1 a8 by simp have a12: "current s = current t" using domain_of_eventR_def a4 by auto have a13: "ta_mgr(TEE_state s) = ta_mgr(TEE_state t)" using a3 vpeq1_def a51 by auto have a14: "?sesID = ?sesID_t" by (simp add: a31) have a15: "?serverID = ?serverID_t" using mgr_ta_sessions_findSesServTid a14 a51 abstract_state_def by simp have a16: "?ses_id = ?ses_id_t" by (simp add: a31) have a17: "?cmd_id = ?cmd_id_t" by (simp add: a31) have a18: "?isSessIdInSessList = ?isSessIdInSessList_t" using isSessIdInTaInsSessList_def a52 using a15 a31 by auto have "(s' ∼. d .∼Δ t')" proof- { have b1: "s' = fst(TEE_InvokeTACommand3R sysconf s)" using exec_eventR_def p1 a7 by simp have b2: "t' = fst(TEE_InvokeTACommand3R sysconf t)" using exec_eventR_def p1 a8 by simp have b3: "current s = current t" using domain_of_eventR_def a4 by simp have b4: "?exec = ?exec_t" by (simp add: a31) show ?thesis proof(cases "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3") case True have c1: "?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3" by (meson True) have c1_1: "?exec_t = [] ∨ ?ses_id_t = None ∨ ?serverID_t = None ∨ current t = TEE sysconf ∨ current t = REE sysconf ∨ current t ≠ ?server_tid_t ∨ snd (hd (exec_prime t)) ≠ TEE_IC3" using a15 b3 b4 c1 by auto have c2: "s' = s" using c1 b1 TEE_InvokeTACommand3R_def by (smt (z3) prod.collapse prod.inject) have c3: "t' = t" using c1 b2 b3 b4 TEE_InvokeTACommand3R_def a31 c1_1 by (smt (z3) State.fold_congs(6) old.prod.inject prod.collapse) then show ?thesis using a3 c2 vpeqR_def by blast next case False have c4: "¬(?exec = [] ∨ ?ses_id = None ∨ ?serverID = None ∨ current s = TEE sysconf ∨ current s = REE sysconf ∨ current s ≠ ?server_tid ∨ snd (hd (exec_prime s)) ≠ TEE_IC3)" using False by auto have c5: "is_TA sysconf (current s)" using is_TA_def by (metis c4) then show ?thesis proof(cases "d = TEE sysconf") case True then show ?thesis using a5 c5 domain_of_eventR_def by force next case False have c6:"d ≠ TEE sysconf" by (simp add: False) then show ?thesis proof(cases "d = REE sysconf") case True then show ?thesis using a5 c5 using domain_of_eventR_def by force next case False have c7:"is_TA sysconf d" using is_TA_def c6 using False by auto have c8:"(s' ∼. d .∼Δ t') =True" using c6 is_TEE_def vpeq_ipc_def by presburger then show ?thesis by auto qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) Pair_inject) qed lemma TEE_InvokeTACommand3R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_INVOKETACOMMAND3))" using TEE_InvokeTACommand3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) subsubsection "TEE_InvokeTACommand4R" lemma TEE_InvokeTACommand4R_integrity: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND4)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof- { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst (TEE_InvokeTACommand4R sysconf s)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEE_InvokeTACommand4R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_InvokeTACommand4R_integrity_e: "integrity_new_e (hyperc' (TEE_INVOKETACOMMAND4))" using TEE_InvokeTACommand4R_integrity integrity_new_e_def by metis lemma TEE_InvokeTACommand4R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_INVOKETACOMMAND4)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof- { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_InvokeTACommand4R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_InvokeTACommand4R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_InvokeTACommand4R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_InvokeTACommand4R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_INVOKETACOMMAND4))" using TEE_InvokeTACommand4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) end